$\forall$${\it es}$:ES, $X$:AbsInterface(Top), $f$:(E($X$)$\rightarrow$E($X$)).
\\[0ex]($\forall$$x$:E($X$). $f$($x$) c$\leq$ $x$)
\\[0ex]$\Rightarrow$ ($\forall$$e$:E($X$). prior{-}$f${-}fixedpoints($e$) $\in$ (\{${\it e'}$:E($X$)$\mid$ $f$(${\it e'}$) = ${\it e'}$ $\in$ E\}  List))